1. $i$ : $\mathbb{N}$
\\[0ex]2. $f$ : \{$f$ $\mid$ $i$:\{$i_{1}$:$\mathbb{N}\mid$ $i_{1}$ ($\lambda$$i$,$j$. $i$ $<$ $j$) $i$\}  $\rightarrow$ if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi \}
\\[0ex]3. $\forall$$j$:\{$k$:$\mathbb{N}\mid$ $k$ $<$ $i$\} . $f$($j$) $\in$ $\mathbb{Z}$
\\[0ex]4. $i$ $\neq$ 0
\\[0ex]$\vdash$  \{$f$($i$ {-} 1)$\ldots\,$\}